Inference at * 2 2 
Iof proof for Lemma p-fun-exp-add-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
9. (n = 0)
  (f^n+m(x)) ~ (f^n(do-apply(f^m;x))) 

latex

 by ((Unfold `p-fun-exp` ( 0)) 
CollapseTHEN (RecUnfold `primrec` 0)) 
CollapseTHEN ((
C(RepeatFor (first_nat 3:n) (((if (0) =0 then SplitOnConclITE else SplitOnHypITE (0))) 

C(CollapseTHENA (Auto)))) 
CollapseTHEN (((Try ((Complete (Auto'))))) 
CollapseTHEN ((
CReduce 0) 
CollapseTHEN (Fold `p-fun-exp` 0)))) 

latex

C1: 

C1: 10. (n+m = 0)
C1: 11. (n = 0)
C1: 12. (m = 0)
C1:   (f o f^(n+m) - 1  (x)) ~ (f o f^n - 1  (do-apply(f o f^m - 1  ;x)))
C.

Definitions	f^n, n+m, left + right, Unit, P  Q, P & Q, x:A  B(x), x:AB(x), (i = j), , b, , A, False, f(a), x.A(x), primrec(n;b;c), f o g  , p-id(), n - m, SQType(T), P  Q, b, , {x:A| B(x)} , {T}, s ~ t, x:A. B(x), , s = t, t  T
Lemmas	bool wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bnot wf, not wf, assert wf